a:, b:. (|a| = |b|  )  ((a rem b) = 0) 

latex

Up	int 2, int 2
Definitions	, t  T, P  Q, x:A. B(x), T, ff, P  Q, P & Q, tt, if b then t else f fi , P  Q, |i|, True, False, A, a  b  T , , , , Unit, , P  Q, Dec(P), A  B,
Lemmas	int nzero wf, nat plus wf, nat wf, absval wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, decidable le, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf, rem eq args, nequal wf, rem antisym, minus mono wrt eq, rem sym